The invention belongs to artificial intelligence which is a subfield of computer science. It relates to a computer system which has a memory for storing programs including knowledge. By means of controlling adjustments it adapts its programs to input signals and generates output signals on the basis of the adapted programs. The input signals can be generated by keyboards or sensors and the output signals can control printers, displays, or the movements of robots.
The efficiency of systems of xe2x80x9cartificial intelligencexe2x80x9d is still very small compared to the capabilities of xe2x80x9chuman intelligencexe2x80x9d. This shall be illustrated in the field of automated theorem proving.
The objective of the field of automated theorem proving is to develop computer systems, so-called theorem provers, which automatically generate proofs of mathematical theorems. After more than thirty years of research and development the efficiency of theorem provers is still trivial compared to the capabilities of mathematicians (see Bundy, A., The Computer Modelling of Mathematical Reasoning, San Diego, Calif.: Academic Press, 1983, p. 10). A well-known problem in automated theorem proving is SAM""s Lemma. The Markgraf Karl Refutation Procedure is one of the greatest projects in the history of automated theorem proving (see Blxc3xa4sius, K., Eisinger, N., Siekmann, J., Smolka, G., Herold, A., and Walther, C., The Markgraf Karl Refutation Procedure, Proceedings of the Seventh International Joint Conference on Artificial Intelligence, August 1981, Vancouver, Canada). After some fifteen years of development Ohlbach and Siekmann give SAM""s Lemma as the only more difficult theorem the Markgraf Karl Refutation Procedure has proved. But a proof of SAM""s Lemma is rather trivial from a mathematician""s point of view because the proof consists of eight equations seven of which simplify the right side of the first equation (see Ammon, K., Proceedings of the Seventh National Conference on Artificial Intelligence, Aug. 21-26, 1988, St. Paul, USA).
The most known procedure in the field of automated theorem proving is the resolution procedure. The theorem prover OTTER 2.2, which is often regarded as the most powerful resolution prover, is also capable of proving SAM""s Lemma (McCune, W. W., OTTER 2.0 Users Guide, Report ANL-90/9, Argonne National Laboratory, Argonne, Ill., 1990, and McCune, W. W., What""s new in OTTER 2.2. Report ANL/MCS-TM-153, Argonne National Laboratory, Argonne, Ill., 1991). But in the proof of SAM""s Lemma the Markgraf Karl Refutation Procedure and OTTER 2.2 do not satisfy the important minimal requirement that a theorem prover should be capable of processing all axioms. For example, the set of axioms in McCharen, J. D., Overbeek, R. A., and Wos, L. A., Problems and experiments for and with automated theorem-proving programs, IEEE Transactions on Computers, Vol. C-25, No. 8, pp. 773-782, is not complete because it does not contain the ordinary lattice operations xe2x80x9cjoinxe2x80x9d and xe2x80x9cmeetxe2x80x9d, that is, the existence of a minimum and a maximum in McCharen et al.""s representation. If these most elementary axioms are given to the system, the theorem prover OTTER 2.2 breaks down in a combinatorial explosion. This means that OTTER 2.2 is not capable of proving SAM""s Lemma because the proof is largely given to the system by a manual selection of the axioms. For the Markgraf Karl Refutation Procedure a proof of SAM""s Lemma is even more difficult than for OTTER 2.2.
Conventional theorem provers such as the Karl Refutation Procedure and OTTER 2.2 have to be controlled manually by so-called options (McCune, W. W., OTTER 2.0 Users Guide, Report ANL-90/9, Argonne National Laboratory, Argonne, Ill., 1990). Because these theorem provers are extensive programs which contain many complex procedures and require powerful computers, a manual control of these options is extremely difficult. This difficulty is even increased by the fact that the procedures in these theorem provers are very different from human reasoning processes, that is, the reasoning processes of the users of these theorem provers. Furthermore, theorem proving problems must be manually translated into a form that can be processed by these theorem provers. For example, the proof of SAM""s Lemma requires a translation of the lattice operations into minimum and maximum relations. Such a manual translation of a theorem can be more difficult than a manual proof of the theorem. Furthermore, it is not known in advance into which representation a theorem must be translated so that a theorem prover can find a proof. Furthermore, conventional theorem provers produce unreadable proofs which must be manually retranslated into a readable form.
Conventional theorem provers are not capable of generating the central ideas of significant theorems in higher mathematics, for example a proof of Gxc3x6del""s Incompleteness Theorem. Even if these ideas are given to a conventional theorem prover, it breaks down after few simple steps in an combinatorial explosion because it cannot process all definitions and lemmas required for proving significant theorems (vgl. Bledsoe, W. W., Non-resolution theorem proving, Artificial Intelligence, Vol. 9, 1977, p. 27). Newer approaches to the development of theorem provers, for example the technology of expert systems, have hardly been applied or did not yield better results. Thus, the capabilities of conventional theorem provers are limited to trivial marginal subfields of mathematics.
An essential property of conventional theorem provers is that they contain many complex and extensive procedures which cannot adapt themselves to hardly predictable new problems and situations. Thus, these theorem provers produce many useless steps and finally break down in a combinatorial explosion because they cannot find new ways if a chosen way does not solve a problem.
The problems and limits of the capabilities described above are not restricted to the field of automated theorem proving. Rather, they apply to systems in other fields of artificial intelligence such as image and language processing and robotics.
The object of the invention is to provide a user-friendly, economical and efficient computer system having a memory for storing knowledge and programs which can also be used in fields that require the solution of new and hardly predictable problems.
According to the invention, this object is achieved by the computer system described subsequently. It processes input signals and finally generates output signals with the aid of the programs and the knowledge in its memory wherein the input and the output signals represent information. It is called adaptive because it is capable of adapting its programs and its knowledge to hardly predictable new problems. An adaptive computer system contains control components and execution components. The control components control the execution components in so-called adjustments. In this process resources are withdrawn from execution components that cannot solve a problem. The withdrawal of resources can be carried out in different ways, for example, completely, partially or temporarily. The withdrawal of resources can also be achieved in that an execution components terminates of itself without result. An important advantage of adaptive computer systems is that they can, by means of adjustments, select execution components that are suitable for solving a problem. Thus, the application of execution components that are not useful for solving a problem is largely avoided. This entails that adaptive computer systems can select and organize a tailored set of efficient execution components which are suitable for solving a problem.
An adaptive computer system is capable of adapting itself to unpredictable new situations, that is, situations that cannot in advance be described completely and in all details. It is capable of generating variations of execution components and then activating these components. It is particularly efficient if in adjustments, it first activates execution components that are simple or require few resources. This efficiency is particularly great if execution components satisfying these two properties, that is, which are simple and require few resources, are activated first. This way of activating execution components has the advantage that an adaptive computer system can be efficient as well as general. The efficiency is achieved by first activating execution components that require few resources. The generality is achieved by then activating more general execution components. Another advantage of this way of activating execution components is that control and execution components can have a simple structure and thus the computer system can be used easily. An adaptive computer system is capable of generating methods for solving problems by composing elementary concepts. It can contain control components that reduce the goal to solve a problem to the subgoal to solve one or more other problems. In adjustments, a control component of an adaptive computer system can control several control components which, in adjustments, control further control components or execution components. This yields the advantage that control and execution components can have a simple structure and thus the computer system can be used easily. An adaptive computer system can select the knowledge required for solving a problem from a knowledge base. This yields the advantage that such a system can also efficiently process great sets of knowledge and does not apply knowledge that is not useful for solving a problem. In an adjustment, an adaptive computer system can allocate more resources to an execution component that produces intermediate results. In this way, its efficiency increases because execution components that are less useful for solving a problem consume less resources. An adaptive computer system can contain a control component which, in several adjustments having a cyclic structure, is activated by a control component it itself has activated.